1. Field
The embodiment relates to a technology of equivalence verification.
2. Description of the Related Art
In the design of integrated circuits, a synchronizer for compensating timing is inserted in a (asynchronous) path between two flip-flops driven by different asynchronous clock signals to avoid metastability. Generally, a synchronizer includes one or more flip-flops. A signal input to a flip-flop is delayed by one clock and output. Hence, even when the flip-flop is inserted in the asynchronous path, it does not affect the logic values of other combinational circuits.
FIG. 1 is a schematic of a typical algorithm indicative of two circuits to be subjected to logic equivalence verification. In a reference circuit 1, a first logic cone 4 is coupled to a second logic cone 8 to which a third logic cone 10 and a sixth logic cone 11 are coupled. The first logic cone 4 starts from an output port of the reference circuit 1 and includes a first combinational circuit 2. The second logic cone 8 starts from input terminals of a flip-flop to be deleted after the merge process A (FF_A) 3 and includes a second combinational circuit 5. The third logic cone 10 starts from input terminals of a flip-flop to remain after the merge process B (FF_B) 6 and includes a third combinational circuit 9. The sixth logic cone 11 starts from input terminals of a third flip-flop C (FF_C) 7. The second and the third flip-flops (FF_B) 6 and (FF_C) 7 are driven by a clock signal F (CLK_F). The flip-flop to be deleted after the merge process (FF_A) 3 is driven by a clock signal G (CLK_G).
In an implemented circuit 21, a fourth and a fifth flip-flops D (FF_D) 22 and E (FF_E) 23 are inserted in an asynchronous path between the second combinational circuit 5 and the flip-flop to be deleted after the merge process (FF_A) 3. The fourth and the fifth flip-flops (FF_D) 22 and (FF_E) 23 are driven by the click signal G (CLK_G). A fourth logic cone 24 that starts from the input terminals of the flip-flop to be deleted after the merge process (FF_A) 3 is coupled to the first logic cone 4. A fifth logic cone 25 that starts from input terminals of the fourth flip-flop (FF_D) 22 is coupled to the fourth logic cone 24. The second logic cone 8 that starts from input terminals of the fifth flip-flop (FF_E) 23 is coupled to the fifth logic cone 25.
Inverters 26 and 27, buffers 28 to 30 may be inserted between the fourth flip-flop (FF_D) 22 and the fifth flip-flop (FF_E) 23. In the logic equivalence verification, the logic cones having an identical name between the reference circuit 1 and the implemented circuit 21 are paired, and verification between the logic cones of the two circuits is performed. When all the logic cones logically match each other, it is judged that the reference circuit 1 and the implemented circuit 21 are logically identical. Generally, a logic cone is a unit block for logic equivalence verification; starts from an output terminal, input terminals of a flip-flop, or an input pin of a black box module; and ends at an input terminal, an output terminal of a flip-flop, or an output pin of a black box module.
A logic-equivalence verification method has been disclosed for the case in which among two logics subjected to the logic equivalence verification, one of the logic includes an additional logic that is not included in the other logic. In the method, equivalence between the logic from which the additional logic is deleted and the other logic is verified based on information concerning the additional logic (see, for example, Japanese Patent Application Laid-open Publication No. 2001-67379).
However, according to the conventional logic-equivalence verification method, since the elements having an identical name are paired to compare logic cones with each other, mismatch occurs between the second logic cone 8 that starts from the input terminal of the flip-flop to be deleted after the merge process (FF_A) 3 and the fourth logic cone 24 though the reference circuit 1 and the implemented circuit 21 are logically identical in the case of FIG. 1. In this case, a designer has to check each part at which an error is detected as a mismatch, or add, to a specification file, information indicating that the fifth flip-flop (FF_E) 23 in the implemented circuit 21 and the flip-flop to be deleted after the merge process (FF_A) 3 in the reference circuit 1 are paired. Such manual operations are troublesome, time consuming, and may lead to mistakes. Furthermore, in the method disclosed in Japanese Patent Application Laid-open Publication No. 2001-67379, deletion of the additional logic based on information concerning the additional logic is troublesome.